Nuprl Lemma : l_contains_wf
11,40
postcript
pdf
T
:Type,
A
,
B
:(
T
List).
A
B
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
x
.
t
(
x
)
,
x
L
.
P
(
x
)
,
A
B
Lemmas
l
all
wf
,
l
member
wf
origin
T:Type, A, B:(T List). A 
B 
T:Type, A, B:(T List). A B Tx:A. B(x) l)
x. t(x)xL. P(x) B